%% Examples for model checking reduciton by forward random walk


interpretationObjs3579(empty, [objects(location,[s1,s2,s3,s4,d]),objects(truck,[t1,t2]), objects(maxobj,[a,a1])]).

%interpretationObjs3579(empty, [objects(location,[s1,s3,d]),objects(truck,[t1,t2]), objects(maxobj,[a,a1])]).


interpretations3579(empty, [
[[empty,empty(s1),empty(s2)],[not_empty,not_empty(s3),not_empty(s4),not_empty(d)],[tfull,tfull(t1)],[not_tfull,not_tfull(t2)],[tin,tin(t1,d),tin(t2,d)],[not_tin,not_tin(t1,s1),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_tfull],[tfull,tfull(t2),tfull(t1)],[empty,empty(s1),empty(s2)],[not_empty,not_empty(s3),not_empty(s4),not_empty(d)],[tin,tin(t1,d),tin(t2,d)],[not_tin,not_tin(t1,s1),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_empty,not_empty(s4),not_empty(d)],[empty,empty(s3),empty(s1),empty(s2)],[not_tin,not_tin(t1,d),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,s1),tin(t2,d)],[not_tfull],[tfull,tfull(t2),tfull(t1)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_tin,not_tin(t1,s1),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,d),tin(t2,d)],[not_empty,not_empty(s4),not_empty(d)],[empty,empty(s3),empty(s1),empty(s2)],[not_tfull],[tfull,tfull(t2),tfull(t1)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[empty,empty(s3),empty(s2)],[tfull,tfull(t2)],[not_tfull,not_tfull(t1)],[not_empty,not_empty(s1),not_empty(s4),not_empty(d)],[not_tin,not_tin(t1,d),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,s1),tin(t2,d)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_tin,not_tin(t1,s1),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,d),tin(t2,d)],[empty,empty(s3),empty(s2)],[tfull,tfull(t2)],[not_tfull,not_tfull(t1)],[not_empty,not_empty(s1),not_empty(s4),not_empty(d)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_tfull],[tfull,tfull(t1),tfull(t2)],[not_tin,not_tin(t1,s1),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,d),tin(t2,d)],[empty,empty(s3),empty(s2)],[not_empty,not_empty(s1),not_empty(s4),not_empty(d)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_empty,not_empty(d)],[empty,empty(s4),empty(s1),empty(s3),empty(s2)],[not_tin,not_tin(t1,d),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,s1),tin(t2,d)],[not_tfull],[tfull,tfull(t1),tfull(t2)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_tin,not_tin(t1,d),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,s1),tin(t2,d)],[empty,empty(s1),empty(s2)],[not_empty,not_empty(s3),not_empty(s4),not_empty(d)],[tfull,tfull(t1)],[not_tfull,not_tfull(t2)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_empty,not_empty(s4),not_empty(d)],[empty,empty(s1),empty(s3),empty(s2)],[tfull,tfull(t2)],[not_tfull,not_tfull(t1)],[not_tin,not_tin(t1,d),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,s1),tin(t2,d)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_empty,not_empty(d)],[empty,empty(s4),empty(s1),empty(s3),empty(s2)],[not_tin,not_tin(t1,s1),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,d),tin(t2,d)],[tfull,tfull(t2)],[not_tfull,not_tfull(t1)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_tin,not_tin(t1,s1),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,d),tin(t2,d)],[not_empty,not_empty(s4),not_empty(d)],[empty,empty(s1),empty(s3),empty(s2)],[tfull,tfull(t2)],[not_tfull,not_tfull(t1)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_empty,not_empty(d)],[empty,empty(s4),empty(s1),empty(s3),empty(s2)],[not_tin,not_tin(t1,d),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,s1),tin(t2,d)],[tfull,tfull(t2)],[not_tfull,not_tfull(t1)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_tin,not_tin(t1,d),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,s1),tin(t2,d)],[not_tfull],[tfull,tfull(t2),tfull(t1)],[empty,empty(s1),empty(s2)],[not_empty,not_empty(s3),not_empty(s4),not_empty(d)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_tin,not_tin(t1,d),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,s1),tin(t2,d)],[not_tfull],[tfull,tfull(t1),tfull(t2)],[empty,empty(s3),empty(s2)],[not_empty,not_empty(s1),not_empty(s4),not_empty(d)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_empty,not_empty(s4),not_empty(d)],[empty,empty(s3),empty(s1),empty(s2)],[not_tin,not_tin(t1,d),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,s1),tin(t2,d)],[tfull,tfull(t1)],[not_tfull,not_tfull(t2)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[empty,empty(s3),empty(s2)],[tfull],[not_tfull,not_tfull(t1),not_tfull(t2)],[not_empty,not_empty(s1),not_empty(s4),not_empty(d)],[not_tin,not_tin(t1,d),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,s1),tin(t2,d)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_empty,not_empty(s4),not_empty(d)],[empty,empty(s1),empty(s3),empty(s2)],[not_tin,not_tin(t1,s1),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,d),tin(t2,d)],[tfull],[not_tfull,not_tfull(t1),not_tfull(t2)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_tfull,not_tfull(t2)],[tfull,tfull(t1)],[not_empty,not_empty(s4),not_empty(d)],[empty,empty(s1),empty(s3),empty(s2)],[not_tin,not_tin(t1,s1),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,d),tin(t2,d)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_empty,not_empty(s4),not_empty(d)],[empty,empty(s1),empty(s3),empty(s2)],[tfull],[not_tfull,not_tfull(t1),not_tfull(t2)],[not_tin,not_tin(t1,d),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,s1),tin(t2,d)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_empty,not_empty(d)],[empty,empty(s4),empty(s1),empty(s3),empty(s2)],[not_tin,not_tin(t1,s1),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,d),tin(t2,d)],[not_tfull],[tfull,tfull(t1),tfull(t2)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[empty,empty(s4),empty(s3),empty(s2)],[tfull,tfull(t2)],[not_tfull,not_tfull(t1)],[not_empty,not_empty(s1),not_empty(d)],[not_tin,not_tin(t1,d),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,s1),tin(t2,d)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_tin,not_tin(t1,s1),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,d),tin(t2,d)],[empty,empty(s4),empty(s3),empty(s2)],[tfull,tfull(t2)],[not_tfull,not_tfull(t1)],[not_empty,not_empty(s1),not_empty(d)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_tfull],[tfull,tfull(t1),tfull(t2)],[not_tin,not_tin(t1,s1),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,d),tin(t2,d)],[empty,empty(s4),empty(s3),empty(s2)],[not_empty,not_empty(s1),not_empty(d)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_tin,not_tin(t1,d),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,s1),tin(t2,d)],[not_tfull],[tfull,tfull(t1),tfull(t2)],[empty,empty(s4),empty(s3),empty(s2)],[not_empty,not_empty(s1),not_empty(d)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[empty,empty(s2)],[tfull],[not_tfull,not_tfull(t1),not_tfull(t2)],[not_empty,not_empty(s1),not_empty(s3),not_empty(s4),not_empty(d)],[not_tin,not_tin(t1,d),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,s1),tin(t2,d)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_empty,not_empty(s3),not_empty(s4),not_empty(d)],[empty,empty(s1),empty(s2)],[not_tfull,not_tfull(t1)],[tfull,tfull(t2)],[not_tin,not_tin(t1,d),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,s1),tin(t2,d)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_tin,not_tin(t1,s1),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,d),tin(t2,d)],[not_empty,not_empty(s3),not_empty(s4),not_empty(d)],[empty,empty(s1),empty(s2)],[not_tfull,not_tfull(t1)],[tfull,tfull(t2)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[empty,empty(s2)],[tfull,tfull(t2)],[not_tfull,not_tfull(t1)],[not_empty,not_empty(s1),not_empty(s3),not_empty(s4),not_empty(d)],[not_tin,not_tin(t1,d),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,s1),tin(t2,d)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],
[[not_tin,not_tin(t1,s1),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,d),tin(t2,d)],[empty,empty(s2)],[tfull,tfull(t2)],[not_tfull,not_tfull(t1)],[not_empty,not_empty(s1),not_empty(s3),not_empty(s4),not_empty(d)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],[[not_empty,not_empty(d)],[empty,empty(s4),empty(s3),empty(s1),empty(s2)],[not_tin,not_tin(t1,s1),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,d),tin(t2,d)],[tfull,tfull(t1)],[not_tfull,not_tfull(t2)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],[[not_empty,not_empty(d)],[empty,empty(s4),empty(s3),empty(s1),empty(s2)],[not_tin,not_tin(t1,d),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,s1),tin(t2,d)],[tfull,tfull(t1)],[not_tfull,not_tfull(t2)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],[[not_empty,not_empty(s3),not_empty(s4),not_empty(d)],[empty,empty(s1),empty(s2)],[tfull],[not_tfull,not_tfull(t1),not_tfull(t2)],[not_tin,not_tin(t1,d),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,s1),tin(t2,d)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],[[not_empty,not_empty(d)],[empty,empty(s4),empty(s3),empty(s1),empty(s2)],[not_tin,not_tin(t1,s1),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,d),tin(t2,d)],[tfull],[not_tfull,not_tfull(t1),not_tfull(t2)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],[[not_tfull],[tfull,tfull(t1),tfull(t2)],[not_tin,not_tin(t1,s1),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,d),tin(t2,d)],[empty,empty(s2)],[not_empty,not_empty(s1),not_empty(s3),not_empty(s4),not_empty(d)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],[[not_tin,not_tin(t1,d),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,s1),tin(t2,d)],[not_tfull],[tfull,tfull(t1),tfull(t2)],[empty,empty(s2)],[not_empty,not_empty(s1),not_empty(s3),not_empty(s4),not_empty(d)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],[[not_empty,not_empty(d)],[empty,empty(s1),empty(s4),empty(s3),empty(s2)],[tfull],[not_tfull,not_tfull(t1),not_tfull(t2)],[not_tin,not_tin(t1,d),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,s1),tin(t2,d)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],[[not_empty,not_empty(s3),not_empty(s4),not_empty(d)],[empty,empty(s1),empty(s2)],[not_tin,not_tin(t1,s1),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,d),tin(t2,d)],[tfull],[not_tfull,not_tfull(t1),not_tfull(t2)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]]]).


%interpretations3579(empty,[[[not_empty,not_empty(s4)],[empty,empty(s3),empty(s1),empty(s2),empty(d)],[not_tin,not_tin(t1,d),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[tin,tin(t1,s1),tin(t2,d)],[not_tfull],[tfull,tfull(t2),tfull(t1)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],[[not_tfull],[tfull,tfull(t2),tfull(t1)],[empty,empty(s1),empty(s2),empty(d)],[not_empty,not_empty(s3),not_empty(s4)],[tin,tin(t1,d),tin(t2,d)],[not_tin,not_tin(t1,s1),not_tin(t1,s2),not_tin(t1,s3),not_tin(t1,s4),not_tin(t2,s1),not_tin(t2,s2),not_tin(t2,s3),not_tin(t2,s4)],[shop,shop(s1),shop(s2),shop(s3),shop(s4)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s2),not_depot(s3),not_depot(s4)],[eq,eq(s1,s1),eq(s2,s2),eq(s3,s3),eq(s4,s4),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s2),not_eq(s1,s3),not_eq(s1,s4),not_eq(s1,d),not_eq(s2,s1),not_eq(s2,s3),not_eq(s2,s4),not_eq(s2,d),not_eq(s3,s1),not_eq(s3,s2),not_eq(s3,s4),not_eq(s3,d),not_eq(s4,s1),not_eq(s4,s2),not_eq(s4,s3),not_eq(s4,d),not_eq(d,s1),not_eq(d,s2),not_eq(d,s3),not_eq(d,s4),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]]]).





%interpretations3579(empty,[[[not_empty],[empty,empty(s3),empty(s1),empty(d)],[not_tin,not_tin(t1,d),not_tin(t1,s3),not_tin(t2,s1),not_tin(t2,s3)],[tin,tin(t1,s1),tin(t2,d)],[not_tfull],[tfull,tfull(t2),tfull(t1)],[shop,shop(s1),shop(s3)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s3)],[eq,eq(s1,s1),eq(s3,s3),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s3),not_eq(s1,d),not_eq(s3,s1),not_eq(s3,d),not_eq(d,s1),not_eq(d,s3),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]],[[not_tfull],[tfull,tfull(t2),tfull(t1)],[empty,empty(s1),empty(d)],[not_empty,not_empty(s3)],[tin,tin(t1,d),tin(t2,d)],[not_tin,not_tin(t1,s1),not_tin(t1,s3),not_tin(t2,s1),not_tin(t2,s3)],[shop,shop(s1),shop(s3)],[not_shop,not_shop(d)],[depot,depot(d)],[not_depot,not_depot(s1),not_depot(s3)],[eq,eq(s1,s1),eq(s3,s3),eq(d,d),eq(t1,t1),eq(t2,t2),eq(a,a),eq(a1,a1)],[not_eq,not_eq(s1,s3),not_eq(s1,d),not_eq(s3,s1),not_eq(s3,d),not_eq(d,s1),not_eq(d,s3),not_eq(t1,t2),not_eq(t2,t1),not_eq(a,a1),not_eq(a1,a)]]]).


